/* Benchmarks for the PionterC verifier. */

// tree visit

struct tree
{
  int data;
  struct tree* l;
  struct tree* r;
};

/*@ let tree(t) = (t==null) ||
  @  	          (({t}) && tree(t->l) && tree(t->l))
  @ in  tree(t)
  @ end
  @*/
int sum(struct tree * t)
{
  int s, sl, sr;
  s = 0;
  
  if (t==null)
    return s;
  else
  {
    sl = sum(t->l);
    sr = sum(t->r);
    s = (t->data) + sl + sr;
    return s;
  }
}
/*@ tree(t) */